/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package alloytoy;

import edu.mit.csail.sdg.alloy4.A4Reporter;
import edu.mit.csail.sdg.alloy4.ConstList;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4compiler.ast.Command;
import edu.mit.csail.sdg.alloy4compiler.ast.CommandScope;
import edu.mit.csail.sdg.alloy4compiler.ast.Module;
import edu.mit.csail.sdg.alloy4compiler.ast.Sig;
import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Options;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution;
import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod;
import edu.mit.csail.sdg.alloy4graph.DotShape;
import edu.mit.csail.sdg.alloy4graph.DotStyle;
import edu.mit.csail.sdg.alloy4graph.Graph;
import edu.mit.csail.sdg.alloy4graph.GraphEdge;
import edu.mit.csail.sdg.alloy4graph.GraphNode;
import java.awt.Color;
import java.io.*;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.Random;
import java.util.logging.Level;
import java.util.logging.Logger;
import tracetoautomata.DFA;
import tracetoautomata.State;

/**
 * A set of Utilities.
 * @author Daniel
 */
public class Util {

    class Location{
        int x;
        int y;
        public Location(int xpos, int ypos)
        {
            x=xpos; y=ypos;
        }

        @Override
        public String toString(){
            return "x:"+x+"-y:"+y;
        }
    }

    class MiniState{
        String label;
        String id;
        Location locationState;
        Location locationLabel;
        ArrayList<MiniState> states;

        public MiniState(String name, String idS, Location lState, Location lLabel)
        {
            label = name;
            id = idS;
            locationState = lState;
            locationLabel = lLabel;
            states = new ArrayList<MiniState>();
        }

        @Override public boolean equals(Object other) {
            if(!(other instanceof MiniState)) return false;
            return ((MiniState) other).label.equals(this.label);
        }

        @Override
        public String toString() { return this.label; }
    }
    
    private static int count(String filename) throws IOException {
        InputStream is = new BufferedInputStream(new FileInputStream(filename));
        byte[] c = new byte[1024];
        int count = 0;
        int readChars = 0;
        while ((readChars = is.read(c)) != -1) {
            for (int i = 0; i < readChars; ++i) {
                if (c[i] == '\n')
                    ++count;
            }
        }
        return count;
    }

    private MiniState StateListContains(ArrayList<MiniState> states, String label)
    {
        for(MiniState s : states)
        {
            if(s.label.equals(label)) return s;
        }
        return null;
    }

    /**
     * Converts the dotFile into a Uppaal xml.
     * @param dotFile
     * @param outputFile
     * @throws IOException
     */
    public void GraphvizUppaal(String dotFile, String outputFile) throws IOException
    {
        ArrayList<Location> locations = new ArrayList<Location>();
        ArrayList<MiniState> states = new ArrayList<MiniState>();

        int x=0;
        int y=-128;
        int deltaStateNames = 10;
        int deltaStateLocations = 10;
        int lineNumber=count(dotFile)*2;
        if(lineNumber%2!=0) lineNumber+=1;
        lineNumber*=4;
        //Matrix creation
        for(int i=0; i<lineNumber/2; i++)
        {
            y=i*deltaStateLocations;
            x=0;
            for(int j=0; j<lineNumber/2; j++)
            {
                Location l = new Location(x,y);
                x+=deltaStateLocations;
                locations.add(l);
            }
        }
        

        String output = "";
        output +="<?xml version=\"1.0\" encoding=\"utf-8\"?>";
        output +="<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>// Place global declarations here.";
        output +="</declaration><template><name x=\"5\" y=\"5\">Template</name>";
        BufferedReader bout = new BufferedReader(new FileReader(dotFile));
        String line="";
        int c=0;
        Random generator = new Random();
        while ((line = bout.readLine()) != null)
        {
           
           if(line.contains("->"))
           {
               c++;
               String label1 = line.substring(0, line.indexOf("->"));
               String label2 = line.substring(line.indexOf("->")+2, line.length()-1);
               
               MiniState state1 = StateListContains(states,label1);
               MiniState state2 = StateListContains(states,label2);
               //System.out.println(states);
               if(state1==null){
                   //System.out.println(c);
                   int r = generator.nextInt(locations.size());
                   Location l = locations.get(r);
                   locations.remove(r);
                   state1 = new MiniState(label1, "id"+c, l, l );
                   output+="<location id=\"id"+c+"\" x=\""+l.x+"\" y=\""+l.y+"\">";
                   output+="<name x=\""+l.x+"\" y=\""+l.y+"\">"+label1+"</name>";
                   output+="</location>";
                   states.add(state1);
                   c++;
               }

               if(state2==null){
                   int r = generator.nextInt(locations.size());
                   Location l = locations.get(r);
                   locations.remove(r);
                   state2 = new MiniState(label2, "id"+c, l, l );
                   output+="<location id=\"id"+c+"\" x=\""+l.x+"\" y=\""+l.y+"\">";
                   output+="<name x=\""+l.x+"\" y=\""+l.y+"\">"+label2+"</name>";
                   output+="</location>";
                   states.add(state2);
                   c++;
               }

               state1.states.add(state2);
           }
	}

        //MiniState tmp = new MiniState(name, "id"+c, l, Location lLabel);
        for(MiniState s: states)
        {
            for(MiniState st : s.states)
            {
                output+="<transition>";
                output+="<source ref=\""+s.id+"\" />";
                output+="<target ref=\""+st.id+"\" />";
                output+="</transition>";
            }
        }
        
        /*int c=0;
        for(Locations l : locations)
        {
            output +="<location id=\"id"+c+"\" x=\""+l.x+"\" y=\""+l.y+"\"></location>";
            c++;
        }*/
        bout.close();
        output +="</template><system>";
        output +="Process = Template();";
        output +="system Process;</system></nta>";
        PrintWriter pw = new PrintWriter(new FileWriter(outputFile));
        pw.write(output);
        pw.close();
    }

    public static void PrintFile(String fileName) throws IOException{
        BufferedReader bout = new BufferedReader(new FileReader(fileName));
        String line="";
        int c=0;
        while ((line = bout.readLine()) != null)
        {
            c++;
            System.out.println (c+"- "+line);
	}
        bout.close();
    }

    public static boolean EqualList(ArrayList<State> l1, ArrayList<State> l2){
        if(l1.size()!=l2.size()) return false;
        for(int i=0; i<l1.size(); i++)
        {
            if(!l1.get(i).MyEquals(l2.get(i))) return false;
        }
        return true;
    }

    public static ArrayList<String> WriteXML(String filename, A4Reporter rep, int ngrow, int nruns, String dir, String predName) throws Err{
        ArrayList<String> names = new ArrayList<String>();
        File tmpdir = new File(dir);
        tmpdir.mkdir();
        Module world = CompUtil.parseEverything_fromFile(rep, null, filename);
        A4Options options = new A4Options();
        for (Command command: world.getAllCommands()) {
            if(command.toString().indexOf(predName)!=-1){
                for(int j=0; j<=ngrow; j++){
                    CommandScope nscope = new CommandScope(command.scope.get(0).sig,true,j);
                    ArrayList<CommandScope> tmp = new ArrayList<CommandScope>();
                    tmp.add(nscope);
                    ConstList<CommandScope> scopelist = ConstList.make(tmp);
                    Command newC = command.change(scopelist);
                    //System.out.println(newC.toString());
                    A4Solution ans = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), newC, options);
                    //A4Solution next = ans.next();
                    int i=0;
                    if(ans.satisfiable())
                    {
                        do{
                            names.add("run_"+j+"_"+i+".xml");
                            ans.writeXML(dir+"/run_"+j+"_"+i+".xml");
                            ans = ans.next();
                            i++;
                        }while(ans.satisfiable() && i<nruns);
                    }
                }
            }

        }
        return names;
    }

    public static String convertToHex(byte[] data) {
        StringBuffer buf = new StringBuffer();
        for (int i = 0; i < data.length; i++) {
            int halfbyte = (data[i] >>> 4) & 0x0F;
            int two_halfs = 0;
            do {
                if ((0 <= halfbyte) && (halfbyte <= 9))
                    buf.append((char) ('0' + halfbyte));
                else
                    buf.append((char) ('a' + (halfbyte - 10)));
                halfbyte = data[i] & 0x0F;
            } while(two_halfs++ < 1);
        }
        return buf.toString();
    }

    public static boolean deleteDir(File dir) {
        if (dir.isDirectory()) {
            String[] children = dir.list();
            for (int i=0; i<children.length; i++) {
                boolean success = deleteDir(new File(dir, children[i]));
                if (!success) {
                    return false;
                }
            }
        }
        // The directory is now empty so delete it
        return dir.delete();
    }

    private static String findExecutable(String prog) {
        String[] paths = System.getenv().get("PATH").split(File.pathSeparator);
	for (String path : paths) {
            String file = (path == null) ? prog : (path + File.separator + prog);
            if (new File(file).canExecute() && !new File(file).isDirectory()) {
                return file;
            }
        }
	return null;
    }

    /**
     * Generate the png from the dotFile. Depends on graphviz instalation.
     * @param dotFile
     * @param pngFile
     */
    public static void CreatePngFromDot(String dotFile, String pngFile)
    {
        try {
            String prog = findExecutable("dot");
            File tmpDot = new File(dotFile);
            StringBuffer outputTypes = new StringBuffer();
            outputTypes.append(" -T").append("png").append(" -o").append(pngFile+".png");
            String dotCommand = prog + outputTypes + " " + tmpDot.getPath();
            Process process = Runtime.getRuntime().exec(dotCommand, null, new File("."));
            @SuppressWarnings(value = "unused")
            int exitVal = process.waitFor();
        } catch (InterruptedException ex) {
            Logger.getLogger(Util.class.getName()).log(Level.SEVERE, null, ex);
        } catch (IOException ex) {
            Logger.getLogger(Util.class.getName()).log(Level.SEVERE, null, ex);
        }
    }

    /**
     * Receives a signatures and returns a list of all sigs in the sub-class tree.
     * @param topSig
     * @param fileModel
     * @return
     * @throws FileNotFoundException
     * @throws IOException
     */
    public static ArrayList<String> GetSubSigs(String topSig, String fileModel) throws FileNotFoundException, IOException
    {
        ArrayList<String> sigs = new ArrayList<String>();
        sigs.add(topSig);
        AlloyFunctions alloy = new AlloyFunctions();
        
        alloy.initAll(fileModel);
        Module alloyModule = alloy.getModule();
        for(Sig s : alloyModule.getAllReachableSigs())
        {
            Sig.PrimSig tmp = (Sig.PrimSig) s;
            if(tmp!=null)
            {
                if(tmp.parent!=null)
                {
                    String tmpstr ="";
                    if(tmp.parent.label.indexOf("this/")!=-1)
                        tmpstr=tmp.parent.label.substring(5, tmp.parent.label.length());
                    else
                        tmpstr = tmp.parent.label;
                    
                    if(sigs.contains(tmpstr)){
                        String tmp2 = "";
                        if(s.label.indexOf("this/")!=-1)
                            tmp2=s.label.substring(5, s.label.length());
                        else
                            tmp2 = s.label;
                        sigs.add(tmp2);
                    }
                }
            }

        }
        //System.out.println(sigs);
        return sigs;
       

    }

    public static Graph GetGraph(String dotFile) throws FileNotFoundException, IOException
    {
        Graph graph = new Graph(3.);
        BufferedReader bout = new BufferedReader(new FileReader(dotFile));
        String tmp = bout.readLine();
        ArrayList<String> states = new ArrayList<String>();
        ArrayList<GraphNode> nodes = new ArrayList<GraphNode>();
        int id=0;
        while(tmp!=null){
            if(tmp.indexOf("->")!=-1)
            {
                String from = tmp.substring(0,tmp.indexOf("->"));
                String to = tmp.substring(tmp.indexOf("->")+2, tmp.length()-1);
                GraphNode fromNode=null;;
                GraphNode toNode=null;
                if(!states.contains(from)){
                    states.add(from);
                    fromNode = new GraphNode(graph, null, from).set(DotShape.BOX).set(Color.yellow).set(DotStyle.SOLID);
                    nodes.add(fromNode);
                }
                else{
                    int i = states.indexOf(from);
                    fromNode = nodes.get(i);
                }
                if(!states.contains(to)){
                    states.add(to);
                    toNode = new GraphNode(graph, null, to).set(DotShape.BOX).set(Color.yellow).set(DotStyle.SOLID);
                    nodes.add(toNode);
                }
                else{
                    int i = states.indexOf(to);
                    toNode = nodes.get(i);
                    
                }
                GraphEdge edge = new GraphEdge(fromNode,toNode, null, "", null).set(Color.GRAY).set(DotStyle.SOLID);
            }
            tmp=bout.readLine();
        }
        return graph;
    }

    public static String dotToXMLMetamodel(String dotFile) throws FileNotFoundException, IOException{
        String res="";
        res+="<!-- /tmp/alloy4tmp40-daniel/tmp/121505/m.xml -->\n";
        res+="<alloy builddate=\"2011/04/12 14:54 EDT\">\n";
        res+="<instance bitwidth=\"4\" maxseq=\"4\" command=\"show metamodel\" filename=\"/home/daniel/alloyplus/barqueiro.als\" metamodel=\"yes\">\n";
        res+="<sig label=\"seq/Int\" ID=\"0\" parentID=\"1\" builtin=\"yes\">\n";
        res+="</sig>\n";
        res+="<sig label=\"Int\" ID=\"1\" parentID=\"2\" builtin=\"yes\">\n";
        res+="</sig>\n";
        res+="<sig label=\"String\" ID=\"3\" parentID=\"2\" builtin=\"yes\">\n";
        res+="</sig>\n";
        res+="<sig label=\"univ\" ID=\"2\" builtin=\"yes\">\n";
        res+="</sig>\n";
        String relation ="";
        relation +="<field label=\"trans\" ID=\"4\" parentID=\"10\">";

   
        BufferedReader bout = new BufferedReader(new FileReader(dotFile));
        String tmp = bout.readLine();
        ArrayList<String> states = new ArrayList<String>();
        int id=0;
        while(tmp!=null){
            System.out.println(states);
            if(tmp.indexOf("->")!=-1)
            {
                String from = tmp.substring(0,tmp.indexOf("->"));
                String to = tmp.substring(tmp.indexOf("->")+2, tmp.length()-1);
                if(!states.contains(from)){
                    //Plus 5 because the id of the relation is 4.
                    res+="<sig label=\""+from+"\" ID=\""+(states.size()+5)+"\" parentID=\"2\">\n";
                    res+="</sig>\n";
                    states.add(from);
                }
                if(!states.contains(to)){
                    res+="<sig label=\""+to+"\" ID=\""+(states.size()+5)+"\" parentID=\"2\">\n";
                    res+="</sig>\n";
                    states.add(to);
                }
                //We have to add the offset in order to get the correct id.
                relation+="<types> <type ID=\""+(states.indexOf(from)+5)+"\"/> <type ID=\""+(states.indexOf(to)+5)+"\"/> </types>\n";
            }

            tmp=bout.readLine();
        }
        relation+="</field>\n";
        res+=relation;
        res+="</instance>\n";
        res+="</alloy>\n";
        return res;
    }


    public static String BuildCompleteDFA(String dirFiles, ArrayList<String> fileNames, ArrayList<String> stateSigs, String graphDir) throws Err
    {
        String fileName=null;
        
        XMLParser parserInit = new XMLParser(dirFiles+fileNames.get(0));
        DFA autoInit = parserInit.parseFileToStates(stateSigs);
        File tmpdir = new File(graphDir);
        tmpdir.mkdir();
        
        autoInit.PrintViz(graphDir+"/"+fileNames.get(0)+".gv");
        //fileName = graphDir+"/"+fileNames.get(0)+".gv";
        
        for(int i=0; i<fileNames.size(); i++)
        {
            XMLParser parseri = new XMLParser(dirFiles+fileNames.get(i));
            DFA autoi = parseri.parseFileToStates(stateSigs);
            autoInit.UniteDFA(autoi);
            autoInit.MinimizeDFA();
            autoInit.PrintViz(graphDir+"/"+fileNames.get(i)+".gv");
            fileName = graphDir+"/"+fileNames.get(i)+".gv";
        }
        return fileName;
    }

    /**
     * Extracts "ClassName" from lines of type
     * <owl:Class rdf:about="&ACC_System;ClassName">
     * @param line
     * @return
     */
    public static String ExtracClassName(String line){
        String tmp = line.substring(25,line.length());
        if(tmp.indexOf(";")!=-1)
            return tmp.substring(tmp.indexOf(";")+1, tmp.length()-2);
        else return null;
    }

    /**
     * Extracts "SuperClass" from lines of type
     * <rdfs:subClassOf rdf:resource="&ACC_System;SuperClass"/>
     * @param line
     * @return
     */
    public static String ExtractSuperClass(String line){
        String tmp = line.substring(29,line.length());
        if(tmp.indexOf(";")!=-1)
            return tmp.substring(tmp.indexOf(";")+1, tmp.length()-3);
        else return null;
    }

    public static String ProcessClass(String line, BufferedReader breader) throws IOException
    {
        String header="";
        String body="";
        header +="sig " + ExtracClassName(line);
        line=breader.readLine();
        boolean extendsDone=false;
        while(line.indexOf("</owl:Class>")==-1)
        {
            
            if(line.indexOf("<rdfs:subClassOf rdf:resource=")!=-1)
            {
                String superClass = ExtractSuperClass(line);
                header +=" extends "+superClass+"{ ";
                extendsDone=true;
            }
            line = breader.readLine();
        }
        if(!extendsDone) header+=" extends Thing{ ";
        body+="}\n";
        return header+body;
    }

    public static void OWLtoAlloy(String owlFile, String alloyFile) throws FileNotFoundException, IOException{
        BufferedReader bout = new BufferedReader(new FileReader(owlFile));
        String line="";
        String output="";
        int c=0;
        output+="sig Thing{}\n\n";
        while ((line = bout.readLine()) != null)
        {
            if(line.indexOf("<owl:Class rdf:about=")!=-1)
            {
                output+= ProcessClass(line,bout);
                
            }
            //output +="sig Cenas extends Thing{}\n";
        }
        output+="\n";
        PrintWriter pw = new PrintWriter(new FileWriter(alloyFile));
        pw.write(output);
        pw.close();
    }
}